(in-package "ACL2")

(defund trim-aux (x)
    (declare (xargs :guard (character-listp x)))
    ;; Remove all whitespace characters from the front of a list.
    (if (consp x)
        (if (or (eql (car x) #\Space)
                (eql (car x) #\Tab)
                (eql (car x) #\Newline)
                (eql (car x) #\Page))
            (trim-aux (cdr x))
          x)
      nil))

(defthm character-listp-of-trim-aux
  (implies (force (character-listp x))
           (character-listp (trim-aux x)))
  :hints(("Goal" :in-theory (enable trim-aux))))

(defthm true-listp-when-character-listp
         (implies (character-listp x)
                  (true-listp x)))

(defund trim (x)
    (declare (xargs :guard (stringp x)))
    (let* ((chars (coerce x 'list))
           (chars (trim-aux chars)) ;; eat spaces at the front
           (chars (reverse chars))  ;; flip so we can get to the back
           (chars (trim-aux chars)) ;; eat spaces at the back
           (chars (reverse chars))) ;; flip again so it's back to normal
      (coerce chars 'string)))

(defthm stringp-of-trim
  (stringp (trim x))
  :hints(("Goal" :in-theory (enable trim)))
  :rule-classes ((:rewrite)
                 (:type-prescription)))

(defun trim-list-of-strs (strs)
   (declare (xargs :guard (string-listp x)))
    ;; Remove all whitespace characters from the front of a list.
    (if (consp strs)
        (cons (trim (car strs))
              (trim-list-of-strs (cdr strs)))
        nil))
